Lawvere Theories

Definition

• from Categorical System Theory
• 

Universal property

• cartesian functors out of it correpond to models of the theory
  • If this is the case, we say that the Lawvere theory is presented by the algebraic theory.
• Definition of a model of a Lawere theory \(\mathcal{L}\) in a cartesian category \(\mathcal{C}\)
  • A model of a Lawere theory \(\mathcal{L}\) in a cartesian category \(\mathcal{C}\) is a cartesian functor \(M: \mathcal{L} \to \mathcal{C}\)
• We say that a Lawvere theory is presented by an algebraic theory if they have the same models in any cartesian category.

• Lawvere theories arise whenever one has a functor into a category with finite products and one studies the natural transformations between finite products of the functor
• Equational theories are a form of presentation for Lawvere theories